$\forall$${\it ds}_{1}$,${\it ds}_{2}$:fpf(Id; $x$.Type).
\\[0ex]fpf{-}sub(Id; $x$.Type; id{-}deq; ${\it ds}_{2}$; ${\it ds}_{1}$) $\Rightarrow$ subtype\_rel(decl{-}state(${\it ds}_{1}$); decl{-}state(${\it ds}_{2}$))